perm filename CONTEX.XGP[S76,JMC] blob
sn#217778 filedate 1976-05-31 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXI30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=XMAS25/FONT#8=FIX25
␈↓ α∧␈↓α␈↓ ∧sCONTEXT DEPENDENT SEMANTICS
␈↓ α∧␈↓␈↓ αTThere␈α∀is␈α∀a␈α∪parallel␈α∀among␈α∀oblique␈α∀contexts␈α∪in␈α∀philosophical␈α∀logic,␈α∀context␈α∪dependent
␈↓ α∧␈↓grammar␈α∩(about␈α∩which␈α∩I␈α∪know␈α∩little),␈α∩the␈α∩FSUBR␈α∪mechanism␈α∩in␈α∩LISP,␈α∩and␈α∪call-by-ame␈α∩in
␈↓ α∧␈↓ALGOL. We hope to treat them uniformly using notions of context-dependent semantics.
␈↓ α∧␈↓␈↓ αTThe␈αidea␈αis␈αsimple.␈α Let␈αus␈αbegin␈αwith␈αthe␈αordinary␈αcontext-free␈αsemantics␈αof␈αterms␈αin␈αfirst
␈↓ α∧␈↓order␈αlogic.␈α Let␈α
␈↓↓f␈↓␈αbe␈αa␈α
function␈αsymbol␈αof␈α
one␈αargument,␈αand␈α
suppose␈αthe␈αinterpretation␈α
␈↓↓I␈↓␈αmaps
␈↓ α∧␈↓into a function ␈↓↓I(f): D → D␈↓. We then have the formula
␈↓ α∧␈↓1)␈↓ αD ␈↓↓value(f[e],I) = I(f)(value(e,I))␈↓
␈↓ α∧␈↓where␈α∩we␈α∪write␈α∩␈↓↓f[e]␈↓␈α∪to␈α∩represent␈α∪the␈α∩symbolic␈α∪application␈α∩of␈α∪the␈α∩function␈α∪symbol␈α∩␈↓↓f␈↓␈α∪to␈α∩the
␈↓ α∧␈↓argument expression ␈↓↓e.␈↓ A simple form of context dependent semantics would replace 1 by
␈↓ α∧␈↓2)␈↓ αD ␈↓↓value(f[e],I) = I(f)(value(e,I'(f)(I))␈↓.
␈↓ α∧␈↓The␈α∩only␈α⊃difference␈α∩is␈α∩that␈α⊃the␈α∩interpretation␈α∩used␈α⊃to␈α∩evaluate␈α∩the␈α⊃subexpression␈α∩is␈α∩not␈α⊃the
␈↓ α∧␈↓interpretation␈α(or␈αenvironment␈α-␈αto␈αuse␈αthe␈α
computer␈αscience␈αterm)␈αof␈αthe␈αouter␈αexpression,␈α
but␈αa
␈↓ α∧␈↓new one that depends on the function symbol ␈↓↓f,␈↓ i.e. on the context of the evaluation of ␈↓↓e.␈↓
␈↓ α∧␈↓␈↓ αTUnfortunately,␈α
the␈α
examples␈α
of␈α
context␈α
dependent␈αsemantics␈α
that␈α
I␈α
have␈α
been␈α
able␈α
to␈αfind
␈↓ α∧␈↓don't take that simple form. Here are four of them.
␈↓ α∧␈↓␈↓ αT1. In modal logic we have
␈↓ α∧␈↓3)␈↓ αD ␈↓↓value(Nec e,W) = ∀W'.(A(W,W') ⊃ value(e,W'))␈↓.
␈↓ α∧␈↓Here ␈↓↓W␈↓ is a possible world and ␈↓↓A(W,W')␈↓ means that ␈↓↓W'␈↓ is a possible world accesible from ␈↓↓W.␈↓
␈↓ α∧␈↓instead␈α
of␈α
a␈α
single␈αaltered␈α
interpretation␈α
or␈α
environment␈α
or␈αpossible␈α
world␈α
as␈α
in␈α
the␈αpreliminary
␈↓ α∧␈↓example, we need all possible worlds accessible from ␈↓↓W.␈↓
␈↓ α∧␈↓␈↓ αT2.␈αNext␈αwe␈αhave␈αpredicate␈αcalculus␈αitself␈α
where␈αwe␈αchose␈αto␈αwrite␈αa␈αquantified␈αexpression␈α
as
␈↓ α∧␈↓␈↓↓All(x,e)␈↓ as a function of a variable ␈↓↓x␈↓ and an expression ␈↓↓e␈↓ instead of writing it ␈↓↓∀x.e.␈↓ We have
␈↓ α∧␈↓4)␈↓ αD ␈↓↓value(All(x,e),I) = ∀x'.(x' ε D ⊃ value(e,assign(x,x',I)))␈↓,
␈↓ α∧␈↓where␈α␈↓↓x␈↓␈α
is␈αthe␈αsymbol␈α
representing␈αa␈αvariable,␈α
␈↓↓x'␈↓␈αranges␈αover␈α
the␈αdomain␈αof␈α
␈↓↓x,␈↓␈αand␈α␈↓↓assign(x,x'I)␈↓␈α
is
␈↓ α∧␈↓the␈α
interpretation␈α
that␈α
results␈α
from␈αassigning␈α
the␈α
value␈α
␈↓↓x'␈↓␈α
to␈αthe␈α
variable␈α
␈↓↓x␈↓␈α
in␈α
the␈αinterpretation
␈↓ α∧␈↓(or environment or state vector I).
␈↓ α∧␈↓␈↓ αT3.␈α⊃Consider␈α⊃a␈α⊃noun␈α⊃such␈α⊃as␈α⊃"criminal"␈α⊃as␈α⊃a␈α⊃predicate,␈α⊃and␈α⊃suppose␈α⊃we␈α⊃want␈α∩to␈α⊃define
␈↓ α∧␈↓"alleged"␈α⊂so␈α⊂that␈α⊂when␈α⊂suitably␈α⊂combined␈α⊂with␈α⊂"criminal"␈α⊂we␈α⊂can␈α⊂get␈α⊂the␈α⊂meaning␈α⊂of␈α∂"alleged
␈↓ α∧␈↓criminal". We write
␈↓ α∧␈↓5)␈↓ αD ␈↓↓value(alleged[e],W) = λx.(value(∃p.lleges(p,e[x]),W))␈↓,
␈↓ α∧␈↓␈↓ ε|1␈↓ ∧
␈↓ α∧␈↓where␈α∞␈↓↓W␈↓␈α∂is␈α∞a␈α∞state␈α∂of␈α∞the␈α∞world,␈α∂and␈α∞␈↓↓alleged[e]␈↓␈α∞is␈α∂again␈α∞a␈α∞predicate␈α∂of␈α∞an␈α∞argument␈α∂␈↓↓x␈↓␈α∞which
␈↓ α∧␈↓asserts that someone alleges ␈↓↓e[x].␈↓
␈↓ α∧␈↓␈↓ αT4. The semantics of conditional expressions is given by
␈↓ α∧␈↓6)␈↓ αD ␈↓↓value(␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b,E) = ␈↓αif␈↓↓ value(p,E) ␈↓αthen␈↓↓ value(a,E) ␈↓αelse␈↓↓ value(b,E)␈↓.
␈↓ α∧␈↓This␈αcan␈αbe␈αput␈αinto␈αgreater␈αparallelism␈αwith␈αthe␈αabove␈αdefinitions␈αby␈αwriting␈αits␈αright␈αhand␈αside
␈↓ α∧␈↓in the form
␈↓ α∧␈↓7)␈↓ αD ␈↓↓(λq.choose(q,value(a,m(q,E)),value(b,m(¬q,E))))(value(p,E))␈↓,
␈↓ α∧␈↓where␈α
␈↓↓choose(p,a,b)␈↓␈α∞is␈α
just␈α∞the␈α
conditional␈α∞expression␈α
␈↓αif␈↓↓␈α
p␈α∞␈↓αthen␈↓↓␈α
a␈α∞␈↓αelse␈↓↓␈α
b␈↓␈α∞again␈α
but␈α∞with␈α
call-by-
␈↓ α∧␈↓value␈α
evaluation,␈αi.e.␈α
all␈αarguments␈α
evaluated␈α
first.␈α The␈α
function␈α␈↓↓m(q,E)␈↓␈α
yields␈α␈↓↓E␈↓␈α
if␈α
the␈αBoolean
␈↓ α∧␈↓variable␈α∂␈↓↓q␈↓␈α∂is␈α∞true,␈α∂but␈α∂yields␈α∂a␈α∞trivial␈α∂environment␈α∂␈↓↓E0␈↓␈α∞if␈α∂␈↓↓q␈↓␈α∂is␈α∂false.␈α∞ ␈↓↓E0␈↓␈α∂has␈α∂the␈α∂property␈α∞that
␈↓ α∧␈↓␈↓↓value(e,E0)␈↓ has some conventional value independent of ␈↓↓e.␈↓
␈↓ α∧␈↓␈↓ αTClearly␈αthese␈αfour␈αexamples␈αhave␈αsomething␈αin␈α
common.␈α It␈αwould␈αbe␈αnice␈αto␈αfind␈αa␈α
general
␈↓ α∧␈↓notion␈α⊃of␈α⊃context␈α⊃dependent␈α⊃semantics␈α⊃that␈α⊃would␈α⊃permit␈α⊃a␈α⊃general␈α⊃context␈α⊃dependent␈α⊂model
␈↓ α∧␈↓theory␈αto␈αbe␈αdefined␈αand␈αstudied.␈α The␈αsimplest␈αoutcome␈αwould␈αbe␈αthat␈αcontext␈αdependent␈αmodel
␈↓ α∧␈↓theory is just the ordinary model theory of a somewhat different class of expressions.
␈↓ α∧␈↓John McCarthy
␈↓ α∧␈↓Stanford Artificial Intelligence Laboratory
␈↓ α∧␈↓Stanford University
␈↓ α∧␈↓Stanford, California 94305
␈↓ α∧␈↓␈↓εThis draft of CONTEX[S76,JMC] PUBbed on May 31, 1976.␈↓
␈↓ α∧␈↓␈↓ ε|2␈↓ ∧